@misc{AIDSLReport2021,
	author = {Geisweiller, Nil and Veitas, Kabir and Asfaw, Eman Shemsu and Roberti, Samuel and Ikle, Matthew and Goertzel, Ben},
	title = {{AI-DSL} {Technical} {Report} ({February} to {May} 2021)},
	url = {https://github.com/singnet/ai-dsl/blob/master/doc/technical-reports/2021-May/ai-dsl-techrep-2021-05_may.pdf},
	year = {2021}
}

@misc{Goertzel2020,
	author = {Ben Goertzel, Nil Geisweiller},
	title = {AI-DSL: Toward a General-Purpose Description Language for AI Agents},
	url = {https://blog.singularitynet.io/ai-dsl-toward-a-general-purpose-description-language-for-ai-agents-21459f691b9e},
	year = {2020}
}

@misc{Geisweiller2017,
	author = {Nil Geisweiller},
	title = {Inference Meta-Learning (part I)},
	url = {https://blog.opencog.org/2017/10/14/inference-meta-learning-part-i/},
	year = {2017}
}

@misc{Geisweiller2018,
	author = {Nil Geisweiller},
	title = {Introspective Reasoning within the OpenCog Framework},
	url = {https://blog.singularitynet.io/introspective-reasoning-within-the-opencog-framework-1bc7e182827},
	year = {2018}
}

@misc{YvesHellenschmidt2002,
	author = {Yves Forkl, Michael Hellenschmidt},
	location = {Kloster Irsee, Germany},
	pages = {17--21},
	publisher = {Fraunhofer Institute},
	series = {Tutorial and Research Workshop on Multi-Modal Dialogue in Mobile Environments},
	url={https://core.ac.uk/display/57029957},
	title = {Mastering agent communication in {EMBASSI} on the basis of a formal ontology},
	year = {2002}
}

@misc{martin_translations_nodate,
	author = {Martin, Philippe},
	file = {Translations between RDF+OWL, N3, KIF, UML, FL, FCG and FE:/home/kabir/Zotero/storage/JQ9VDTGT/comparisons.html:text/html},
	language = {English},
	title = {Translations between {RDF}+{OWL}, {N3}, {KIF}, {UML}, {FL}, {FCG} and {FE}},
	url = {http://www.webkb.org/doc/model/comparisons.html},
	urldate = {2021-05-12}
}

@misc{singularitynet_foundation_phasetwo_2021,
	title = {{SingularityNET Foundation}, {PhaseTwo} {Information} {Memorandum}},
	url = {https://rebrand.ly/SNPhase2},
	language = {English},
	publisher = {SingularityNET Foundation},
	month = feb,
	year = {2021},
}

@inproceedings{brady_resource-dependent_2015,
	address = {Cham},
	title = {Resource-{Dependent} {Algebraic} {Effects}},
	isbn = {978-3-319-14675-1},
	abstract = {There has been significant interest in recent months in finding new ways to implement composable and modular effectful programs using handlers of algebraic effects. In my own previous work, I have shown how an algebraic effect system (called effects) can be embedded directly in a dependently typed host language. Using dependent types ought to allow precise reasoning about programs; however, the reasoning capabilities of effects have been limited to simple state transitions which are known at compile-time. In this paper, I show how effects can be extended to support reasoning in the presence of run-time state transitions, where the result may depend on run-time information about resource usage (e.g. whether opening a file succeeded). I show how this can be used to build expressive APIs, and to specify and verify the behaviour of interactive, stateful programs. I illustrate the technique using a file handling API, and an interactive game.},
	booktitle = {Trends in {Functional} {Programming}},
	publisher = {Springer International Publishing},
	author = {Brady, Edwin},
	editor = {Hage, Jurriaan and McCarthy, Jay},
	year = {2015},
	pages = {18--33},
	file = {Brady.2014.RewourceDependentAlgebraicEffects.pdf:/home/kabir/vveitas@gmail.com/library/ai-dsl/Brady.2014.RewourceDependentAlgebraicEffects.pdf:application/pdf},
}

@article{gruber_translation_1993,
	title = {A translation approach to portable ontology specifications},
	volume = {5},
	issn = {1042-8143},
	url = {https://www.sciencedirect.com/science/article/pii/S1042814383710083},
	doi = {https://doi.org/10.1006/knac.1993.1008},
	abstract = {To support the sharing and reuse of formally represented knowledge among AI systems, it is useful to define the common vocabulary in which shared knowledge is represented. A specification of a representational vocabulary for a shared domain of discourse—definitions of classes, relations, functions, and other objects—is called an ontology. This paper describes a mechanism for defining ontologies that are portable over representation systems. Definitions written in a standard format for predicate calculus are translated by a system called Ontolingua into specialized representations, including frame-based systems as well as relational languages. This allows researchers to share and reuse ontologies, while retaining the computational benefits of specialized implementations. We discuss how the translation approach to portability addresses several technical problems. One problem is how to accommodate the stylistic and organizational differences among representations while preserving declarative content. Another is how to translate from a very expressive language into restricted languages, remaining system-independent while preserving the computational efficiency of implemented systems. We describe how these problems are addressed by basing Ontolingua itself on an ontology of domain-independent, representational idioms.},
	number = {2},
	journal = {Knowledge Acquisition},
	author = {Gruber, Thomas R.},
	year = {1993},
	pages = {199--220},
	file = {Gruber.1993.ATranslationApproachToPortableOntologySpecifications.pdf:/home/kabir/vveitas@gmail.com/library/ai-dsl/Gruber.1993.ATranslationApproachToPortableOntologySpecifications.pdf:application/pdf},
}

@incollection{Hofweber2021,
	author       =	{Hofweber, Thomas},
	title        =	{{Logic and Ontology}},
	booktitle    =	{The {Stanford} Encyclopedia of Philosophy},
	editor       =	{Edward N. Zalta},
	howpublished =	{\url{https://plato.stanford.edu/archives/spr2021/entries/logic-ontology/}},
	year         =	{2021},
	edition      =	{{S}pring 2021},
	publisher    =	{Metaphysics Research Lab, Stanford University}
}

@misc{nunet_nunet_2021,
	title = {{NuNet} architecture and service discovery principles (for {AI}-{DSL})},
	url = {https://www.youtube.com/watch?v=GKH9C8pb3yw},
	urldate = {2021-05-26},
	author = {{NuNet}},
	month = may,
	year = {2021}
}

@misc{gRPC,
	title = {{gRPC}, {gRPC Homepage}},
	url = {https://grpc.io/},
	year = {2021}
}

@misc{Protobuf,
	title = {{Protocol Buffers}, {Protocol Buffers Homepage}},
	url = {https://developers.google.com/protocol-buffers/},
	year = {2021}
}

@misc{SNETExampleService,
	title = {{SingularityNET example service}, {example-service GitHub Repository}},
	url = {https://github.com/singnet/example-service},
	year = {2021}
}

@misc{SNETTutorial,
	title = {{SingularityNET Tutorial}, {SingularityNET Tutorial Webpage}},
	url = {https://dev.singularitynet.io/tutorials/publish},
	year = {2021}
}

@misc{SNETRegistry,
	title = {{SingularityNET Registry}, {SingularityNET Registry Documentation Webpage}},
	url = {https://dev.singularitynet.io/docs/concepts/registry/},
	year = {2021}
}

@misc{AIDSLRelatedWork,
	title = {{AI-DSL Related Work}, {AI-DSL Related Work GitHub Issue 43}},
	url = {https://github.com/singnet/ai-dsl/issues/43},
	year = {2021}
}

@misc{Idris,
	title = {{Idris}, {Idris Homepage}},
	url = {https://www.idris-lang.org/},
	year = {2021}
}

@misc{Vectors,
	title = {{Idris2}, {Idris2 Vectors Documentation}},
	url = {https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html#vectors},
	year = {2021}
}

@misc{AIDSLRepo,
	title = {{AI-DSL}, {AI-DSL GitHub Repository}},
	url = {https://github.com/singnet/ai-dsl/},
	year = {2021}
}

@misc{ExternalToolsRepo,
	title = {{OpenCog External Tools}, {OpenCog External Tools GitHub Repository}},
	url = {https://github.com/opencog/external-tools/},
	year = {2021}
}

@misc{SNETDocumentationServiceSetup,
	title = {{SingularityNET Developer Portal}, {Service Setup Web Page}},
	url = {https://dev.singularitynet.io/docs/ai-developers/service-setup/},
	year = {2021}
}

@misc{NuNetFakeNewsWarningAppRepo,
  title = {{NuNet}, {Program Graph of fake News Warning Application}},
  url = {https://gitlab.com/nunet/fake-news-detection/fake\_news\_score/-/blob/master/service/dag.json},
  year = {2021}
}

@inproceedings{kalibatiene_survey_2011,
	address = {Berlin, Heidelberg},
	title = {Survey on {Ontology} {Languages}},
	isbn = {978-3-642-24511-4},
	booktitle = {Perspectives in {Business} {Informatics} {Research}},
	publisher = {Springer Berlin Heidelberg},
	author = {Kalibatiene, Diana and Vasilecas, Olegas},
	editor = {Grabis, Janis and Kirikova, Marite},
	year = {2011},
	pages = {124--141},
	file = {chp3A10.10072F978-3-642-24511-4_10.pdf:/home/kabir/vveitas@gmail.com/library/ai-dsl/chp3A10.10072F978-3-642-24511-4_10.pdf:application/pdf},
}

@unpublished{pease_standard_2009,
	type = {Technical {Report}},
	title = {Standard {Upper} {Ontology} {Knowledge} {Interchange} {Format}},
	url = {http://ontolog.cim3.net/file/resource/reference/SIGMA-kee/suo-kif.pdf},
	language = {English},
	urldate = {2021-05-04},
	author = {Pease, Adam},
	month = jun,
	year = {2009},
}

@inproceedings{NilesPease2001,
author = {Niles, Ian and Pease, Adam},
title = {Towards a Standard Upper Ontology},
year = {2001},
isbn = {1581133774},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/505168.505170},
doi = {10.1145/505168.505170},
booktitle = {Proceedings of the International Conference on Formal Ontology in Information Systems - Volume 2001},
pages = {2–9},
numpages = {8},
keywords = {ontologies, knowledge interchange format},
location = {Ogunquit, Maine, USA},
series = {FOIS '01}
}

@unpublished{pease_sigma_2001,
	title = {The {Sigma} {Ontology} {Development} {Environment}},
	url = {http://www.ceur-ws.org/Vol-71/Pease.pdf},
	language = {English},
	author = {Pease, Adam},
	year = {2001},
	file = {Pease-IJCAI2003 (1).pdf:/home/kabir/vveitas@gmail.com/library/ai-dsl/Pease-IJCAI2003 (1).pdf:application/pdf},
}

@misc{Baumgartner_automatedreasoning,
    author = {Peter Baumgartner and Fabian M. Suchanek},
    title = {Automated Reasoning Support for SUMO/KIF},
    year = {2005}
}

@misc{Urban_anoverview,
    author = {Josef Urban},
    title = {An Overview of Methods for Large-Theory Automated Theorem Proving},
    year = {2011}
}

@inproceedings{Alvez_evaluating_atp_adimen_SUMO,
	address = {Coimbra, Portugal},
	title = {Evaluating Automated Theorem Provers Using Adimen-SUMO},
	booktitle = {Proceedings of the 3rd Vampire Workshop at the 8th International Joint Conference on Automated Reasoning (IJCAR 2016)},
	publisher = {Springer International Publishing},
	author = {Javier Álvez, Paqui Lucio, German Rigau},
	year = {2016},
}

@inproceedings{SojakovaKristina2009,
author="Sojakova, Kristina and Rabe, Florian",
editor="Corradini, Andrea and Montanari, Ugo",
title="Translating a Dependently-Typed Logic to First-Order Logic",
booktitle="Recent Trends in Algebraic Development Techniques",
year="2009",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="326--341",
abstract="DFOL is a logic that extends first-order logic with dependent types. We give a translation from DFOL to FOL formalized as an institution comorphism and show that it admits the model expansion property. This property together with the borrowing theorem implies the soundness of borrowing --- a result that enables us to reason about entailment in DFOL by using automated tools for FOL. In addition, the translation permits us to deduce properties of DFOL such as completeness, compactness, and existence of free models from the corresponding properties of FOL, and to regard DFOL as a fragment of FOL. We give an example that shows how problems about DFOL can be solved by using the automated FOL prover Vampire. Future work will focus on the integration of the translation into the specification and translation tool HeTS.",
isbn="978-3-642-03429-9"
}

@article{Pease_firstorder,
title = "First order reasoning on a large ontology",
abstract = "We present results of our work on using first order theorem proving to reason over a large ontology (the Suggested Upper Merged Ontology - SUMO), and methods for making SUMO suitable for first order theorem proving. We describe the methods for translating into standard first order format, as well as optimizations that are intended to improve inference performance. We also describe our work in translating SUMO from its native SUO-KIF language into TPTP format.",
author = "Adam Pease and Geoff Sutcliffe",
year = "2007",
month = dec,
day = "1",
language = "English (US)",
volume = "257",
pages = "61--70",
journal = "CEUR Workshop Proceedings",
issn = "1613-0073",
publisher = "CEUR-WS",
note = "21st CADE 2007 Workshop on Empirically Successful Automated Reasoning in Large Theories, ESARLT 2007 ; Conference date: 17-07-2007 Through 17-07-2007",
}

@inproceedings{Altenkirch05whydependent,
    author = {Thorsten Altenkirch and Conor Mcbride and James Mckinna},
    title = {Why dependent types matter},
    booktitle = {In preparation, http://www.e-pig.org/downloads/ydtm.pdf},
    year = {2005}
}

@misc{DTL,
	title = {Wikipedia. Category:Dependently typed languages},
	url = {https://en.wikipedia.org/wiki/Category:Dependently_typed_languages}
}

@misc{Gruber_anontology,
    author = {Thomas R. Gruber and Gregory R. Olsen},
    title = {An Ontology for Engineering Mathematics Abstract},
    year = {1994}
}

@inproceedings{Gruber92towarda,
    author = {Thomas R. Gruber and Jay M. Tenenbaum and Jay C. Weber},
    title = {Toward a Knowledge Medium for Collaborative Product Development},
    booktitle = {In J. S. Gero (Eds.), Artificial Intelligence in Design ‘92},
    year = {1992},
    pages = {413--432},
    publisher = {Kluwer Academic Publishers}
}

@inproceedings{Brazier1995,
author = {Brazier, Frances and Dunin-Keplicz, Barbara and Jennings, Nick and Treur, Jan},
year = {1995},
month = {01},
pages = {25-32},
title = {Formal Specification of Multi-Agent Systems: A Real-World Case.}
}

@article{Bourahla20055,
title = {Formal Specification and Verification of Multi-Agent Systems},
journal = {Electronic Notes in Theoretical Computer Science},
volume = {123},
pages = {5-17},
year = {2005},
note = {Proceedings of the 11th Workshop on Logic, Language, Information and Computation (WoLLIC 2004)},
issn = {1571-0661},
doi = {https://doi.org/10.1016/j.entcs.2004.04.042},
url = {https://www.sciencedirect.com/science/article/pii/S1571066105000447},
author = {Mustapha Bourahla and Mohamed Benmohamed},
keywords = {Agents, Multi-Agent Systems, Multi-Modal Branching-Time Logic, Formal Specification and Verification, Model Checking},
abstract = {Multi-agent systems are increasingly complex, and the problem of their verification and validation is acquiring increasing importance. In this paper we show how a well known and effective verification technique, model checking, can be generalized to deal with multi-agent systems. This paper explores a particular type of multi-agent system, in which each agent is viewed as having the three mental attitudes of belief (B), desire (D), and intention (I). We use a multi-modal branching-time logic BDICTL, with a semantics that is grounded in traditional decision theory and a possible-worlds framework. A preliminary implementation of the approach shows promising results.}
}

@article{Desouky2007,
author = {El-Desouky, Ali and Ali, Hesham and Elghamrawy, Sally},
year = {2007},
month = {04},
pages = {},
title = {A Proposed Architecture for Distributed Multi-Agent Intelligent System (DMAIS)}
}

@article{Roelofs2020,
author = {Roelofs, Martijn and Vos, Roelof},
year = {2020},
month = {12},
pages = {1-25},
title = {Automatically inferring technology compatibility with an ontology and graph rewriting rules},
volume = {32},
journal = {Journal of Engineering Design},
doi = {10.1080/09544828.2020.1860202}
}

@inproceedings{Witherell2009,
author = {Witherell, Paul and Krishnamurty, Sundar and Grosse, Ian and Wileden, Jack},
year = {2009},
month = {01},
pages = {685-697},
title = {FIDOE: A Framework for Intelligent Distributed Ontologies in Engineering},
doi = {10.1115/DETC2008-50099}
}

@misc{SWRL,
	title = {{SWRL: A Semantic Web Rule Language
Combining OWL and RuleML}},
	url = {https://www.w3.org/Submission/SWRL/},
	year = {2004}
}

@misc{KIF,
	title = {{Knowledge Interchange Format (KIF)}},
	url = {http://www-ksl.stanford.edu/knowledge-sharing/kif/},
	year = {2021}
}

@article{Labrou99thecurrent,
    author = {Yannis Labrou and Tim Finin and Yun Peng},
    title = {The current landscape of Agent Communication Languages},
    journal = {INTELLIGENT SYSTEMS},
    year = {1999},
    volume = {14},
    pages = {45--52}
}

@misc{FIPAACL,
	title = {{FIPA-ACL Standard Specification}},
	url = {http://www.fipa.org/repository/standardspecs.html/},
	year = {2012}
}

@misc{FunctionOntology,
	title = {{Function Ontology}, {Function Ontology Homepage}},
	url = {https://fno.io/},
	year = {2021}
}

@article{DeMeester2020,
title = {Implementation-independent function reuse},
journal = {Future Generation Computer Systems},
volume = {110},
pages = {946-959},
year = {2020},
issn = {0167-739X},
doi = {https://doi.org/10.1016/j.future.2019.10.006},
url = {https://www.sciencedirect.com/science/article/pii/S0167739X19303723},
author = {Ben {De Meester} and Tom Seymoens and Anastasia Dimou and Ruben Verborgh},
keywords = {Function, Linked data, Reuse},
abstract = {Functions are essential building blocks of information retrieval and information management. However, efforts implementing these functions are fragmented: one function has multiple implementations, within specific development contexts. This inhibits reuse: metadata of functions and associated implementations need to be found across various search interfaces, and implementation integration requires human interpretation and manual adjustments. An approach is needed, independent of development context and enabling description and exploration of functions and (automatic) instantiation of associated implementations. In this paper, after collecting scenarios and deriving corresponding requirements, we (i) propose an approach that facilitates functions’ description, publication, and exploration by modeling and publishing abstract function descriptions and their links to concrete implementations; and (ii) enable implementations’ automatic instantiation by exploiting those published descriptions. This way, we can link to existing implementations, and provide a uniform detailed search interface across development contexts. The proposed model (the Function Ontology) and the publication method following the Linked Data principles using standards, are deemed sufficient for this task, and are extensible to new development contexts. The proposed set of tools (the Function Hub and Function Handler) are shown to fulfill the collected requirements, and the user evaluation proves them being perceived as a valuable asset during software retrieval. Our work thus improves developer experience for function exploration and implementation instantiation.}
}

@inproceedings{Abbot1995,
author = {Abbott, John and Leeuwen, André and Strotmann, Andreas},
year = {1995},
month = {07},
pages = {},
title = {Objectives of OpenMath: Towards a Standard for Exchanging Mathematical Information}
}

@misc{nevzorova2014ontomathpro,
      title={$OntoMath^{PRO}$ Ontology: A Linked Data Hub for Mathematics},
      author={Olga Nevzorova and Nikita Zhiltsov and Alexander Kirillovich and Evgeny Lipachev},
      year={2014},
      eprint={1407.4833},
      archivePrefix={arXiv},
      primaryClass={cs.AI}
}

@inproceedings{Elizarov2017,
author="Elizarov, Alexander
and Kirillovich, Alexander
and Lipachev, Evgeny
and Nevzorova, Olga",
editor="Kalinichenko, Leonid
and Kuznetsov, Sergei O.
and Manolopoulos, Yannis",
title="Digital Ecosystem OntoMath: Mathematical Knowledge Analytics and Management",
booktitle="Data Analytics and Management in Data Intensive Domains",
year="2017",
publisher="Springer International Publishing",
address="Cham",
pages="33--46",
abstract="A mathematical knowledge management technology is discussed, its basic ideas, approaches and results are based on targeted ontologies in the field of mathematics. The solution forms the basis of the specialized digital ecosystem OntoMath which consists of a set of ontologies, text analytics tools and applications for managing mathematical knowledge. The studies are in line with the project aimed to create a World Digital Mathematical Library whose objective is to design a distributed system of interconnected repositories of digitized versions of mathematical documents.",
isbn="978-3-319-57135-5"
}

@article{DBLP:journals/corr/SeshiaS16,
  author    = {Sanjit A. Seshia and
               Dorsa Sadigh},
  title     = {Towards Verified Artificial Intelligence},
  journal   = {CoRR},
  volume    = {abs/1606.08514},
  year      = {2016},
  url       = {http://arxiv.org/abs/1606.08514},
  archivePrefix = {arXiv},
  eprint    = {1606.08514},
  timestamp = {Mon, 13 Aug 2018 16:48:19 +0200},
  biburl    = {https://dblp.org/rec/journals/corr/SeshiaS16.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{HAND2020100037,
title = {Validating and Verifying AI Systems},
journal = {Patterns},
volume = {1},
number = {3},
pages = {100037},
year = {2020},
issn = {2666-3899},
doi = {https://doi.org/10.1016/j.patter.2020.100037},
url = {https://www.sciencedirect.com/science/article/pii/S2666389920300428},
author = {David J. Hand and Shakeel Khan},
abstract = {AI systems will only fulfill their promise for society if they can be relied upon. This means that the role and task of the system must be properly formulated; that the system must be bug free, be based on properly representative data, and can cope with anomalies and data quality issues; and that its output is sufficiently accurate for the task.}
}

@incollection{MENZIES2005153,
title = {Verification and Validation and Artificial Intelligence},
series = {Advances in Computers},
publisher = {Elsevier},
volume = {65},
pages = {153-201},
year = {2005},
issn = {0065-2458},
doi = {https://doi.org/10.1016/S0065-2458(05)65004-8},
url = {https://www.sciencedirect.com/science/article/pii/S0065245805650048},
author = {Tim Menzies and Charles Pecheur},
abstract = {Artificial Intelligence (AI) is useful. AI can deliver more functionality for reduced cost. AI should be used more widely but won't be unless developers can trust adaptive, nondeterministic, or complex AI systems. Verification and validation is one method used by software analysts to gain that trust. AI systems have features that make them hard to check using conventional V&V methods. Nevertheless, as we show in this chapter, there are enough alternative readily-available methods that enable the V&V of AI software.}
}

@inproceedings{Pineyro2019,
author = {Piñeyro, Leonardo and Pardo, Alberto and Viera, Marcos},
year = {2019},
month = {09},
pages = {46-53},
title = {Structure verification of deep neural networks at compilation time using dependent types},
isbn = {978-1-4503-7638-9},
journal = {SBLP 2019: Proceedings of the XXIII Brazilian Symposium on Programming Languages},
doi = {10.1145/3355378.3355379}
}

@inproceedings{Diehl2011,
author = {Larry Diehl},
year = {2011},
title = {Veriﬁed Stack-Based Genetic Programming via Dependent Types},
journal = {Approaches andApplications of Inductive Programming (AAIP)}
}

@misc{SohamNeural,
	author = {Soham Chowdhury},
	title = {GitHub Gist page of Neural.idr},
	url = {https://gist.github.com/mrkgnao/a45059869590d59f05100f4120595623}
}

@inproceedings{Monads1993,
author="Wadler, Philip",
editor="Broy, Manfred",
title="Monads for functional programming",
booktitle="Program Design Calculi",
year="1993",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="233--264",
abstract="The use of monads to structure functional programs is described. Monads provide a convenient framework for simulating effects found in other languages, such as global state, exception handling, output, or non-determinism. Three case studies are looked at in detail: how monads ease the modification of a simple evaluator; how monads act as the basis of a datatype of arrays subject to in-place update; and how monads can be used to build parsers.",
isbn="978-3-662-02880-3"
}


@inproceedings{EmbedDepth2014,
author = {Gibbons, Jeremy and Wu, Nicolas},
title = {Folding Domain-Specific Languages: Deep and Shallow Embeddings (Functional Pearl)},
year = {2014},
isbn = {9781450328739},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/2628136.2628138},
doi = {10.1145/2628136.2628138},
abstract = {A domain-specific language can be implemented by embedding within a general-purpose host language. This embedding may be deep or shallow, depending on whether terms in the language construct syntactic or semantic representations. The deep and shallow styles are closely related, and intimately connected to folds; in this paper, we explore that connection.},
booktitle = {Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming},
pages = {339–347},
numpages = {9},
keywords = {deep and shallow embedding, folds, domain-specific languages},
location = {Gothenburg, Sweden},
series = {ICFP '14}
}

@misc{OWL,
	title = {OWL 2 Web Ontology Language Document Overview (Second Edition)},
	url = {https://www.w3.org/TR/owl2-overview/},
	year = {2012}
}

@inbook{Goertzel2014EGI1,
author="Goertzel, Ben and Pennachin, Cassio and Geisweiller, Nil",
title="Engineering General Intelligence, Part 1: A Path to Advanced Agi Via Embodied Learning and Cognitive Synergy",
year="2014",
publisher="Atlantis Press",
}

@inbook{Goertzel2014EGI2,
author="Goertzel, Ben and Pennachin, Cassio and Geisweiller, Nil",
title="Engineering General Intelligence, Part 2: The CogPrime Architecture for Integrative, Embodied AGI",
year="2014",
publisher="Atlantis Press",
}

@Inbook{Goertzel2014EGI2Chapt18,
author="Goertzel, Ben and Pennachin, Cassio and Geisweiller, Nil",
title="Engineering General Intelligence, Part 2: The CogPrime Architecture for Integrative, Embodied AGI, Chapter 18: Adaptive, Integrative Inference Control",
year="2014",
publisher="Atlantis Press",
}

@inproceedings{Christiansen2016,
author = {Christiansen, David and Brady, Edwin},
year = {2016},
month = {09},
pages = {284-297},
title = {Elaborator reflection: extending Idris in Idris},
doi = {10.1145/2951913.2951932}
}

@inproceedings{Zhang2020,
author = {Zhang, Ruqi and Li, Chunyuan and Zhang, Jianyi and Chen, Changyou and Wilson, Andrew},
year = {2020},
title = {Cyclical Stochastic Gradient {MCMC} for Bayesian Deep Learning},
series = {ICLR}
}

@article{Solomonoff1964,
author = {Solomonoff, Ray},
year = {1964},
title = {A Formal Theory of Inductive Inference},
volume = {7},
journal = {Information and Control}
}

@book{Goertzel09PLN,
title = {Probabilistic Logic Networks},
subtitle = {A Comprehensive Framework for Uncertain Inference},
author = {Goertzel, Ben and Ikle, Matthew and Goertzel, Izabela Freire and Heljakka, Ari},
year = {2009},
publisher = {Springer US}
}

@inproceedings{Menisov2022,
author = {Menisov Artem},
year = {2022},
title = {An approach to generation triggers for parrying backdoor in neural networks},
series = {AGI}
}

@article{DBLP:journals/corr/SelsamLD17,
  author    = {Daniel Selsam and
               Percy Liang and
               David L. Dill},
  title     = {Developing Bug-Free Machine Learning Systems With Formal Mathematics},
  journal   = {CoRR},
  volume    = {abs/1706.08605},
  year      = {2017},
  url       = {http://arxiv.org/abs/1706.08605},
  eprinttype = {arXiv},
  eprint    = {1706.08605},
  timestamp = {Mon, 13 Aug 2018 16:48:35 +0200},
  biburl    = {https://dblp.org/rec/journals/corr/SelsamLD17.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{Lean,
  author = {Leonardo de Moura and Soonho Kong and Jeremy Avigad and Floris van Doorn and Jakob von Raumer},
  title = The Lean Theorem Prover,
  year = {2015},
  booktitle = {Automated Deduction - CADE-25, 25th International Conference
               on Automated Deduction, Berlin, Germany, August 1-7, 2015,
               Proceedings},
  documenturl = {http://leodemoura.github.io/files/lean_cade25.pdf}
}

@article{Hoeffding1963,
 ISSN = {01621459},
 URL = {http://www.jstor.org/stable/2282952},
 abstract = {Upper bounds are derived for the probability that the sum S of n independent random variables exceeds its mean ES by a positive number nt. It is assumed that the range of each summand of S is bounded or bounded above. The bounds for $\Pr \{ S - ES \geq nt \}$ depend only on the endpoints of the ranges of the summands and the mean, or the mean and the variance of S. These results are then used to obtain analogous inequalities for certain sums of dependent random variables such as U statistics and the sum of a random sample without replacement from a finite population.},
 author = {Wassily Hoeffding},
 journal = {Journal of the American Statistical Association},
 number = {301},
 pages = {13--30},
 publisher = {[American Statistical Association, Taylor & Francis, Ltd.]},
 title = {Probability Inequalities for Sums of Bounded Random Variables},
 urldate = {2022-11-11},
 volume = {58},
 year = {1963}
}

@article{Ramananandro2016,
  title={A unified Coq framework for verifying C programs with floating-point computations},
  author={Tahina Ramananandro and Paul Mountcastle and Beno{\^i}t Meister and Richard A. Lethin},
  journal={Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs},
  year={2016}
}

@inproceedings{Harrison2006,
  title={Floating-Point Verification Using Theorem Proving},
  author={John Harrison},
  booktitle={SFM},
  year={2006}
}

@article{Bagnall2019,
author = {Bagnall, Alexander and Stewart, Gordon},
year = {2019},
month = {07},
pages = {2662-2669},
title = {Certifying the True Error: Machine Learning in Coq with Verified Generalization Guarantees},
volume = {33},
journal = {Proceedings of the AAAI Conference on Artificial Intelligence},
doi = {10.1609/aaai.v33i01.33012662}
}

@inproceedings{Bertot2004,
  title={Interactive Theorem Proving and Program Development},
  author={Yves Bertot and Pierre Cast{\'e}ran},
  booktitle={Texts in Theoretical Computer Science An EATCS Series},
  year={2004}
}

@article{Bernardo2019,
  author    = {Bruno Bernardo and
               Rapha{\"{e}}l Cauderlier and
               Zhenlei Hu and
               Basile Pesin and
               Julien Tesson},
  title     = {Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts},
  journal   = {CoRR},
  volume    = {abs/1909.08671},
  year      = {2019},
  url       = {http://arxiv.org/abs/1909.08671},
  eprinttype = {arXiv},
  eprint    = {1909.08671},
  timestamp = {Tue, 24 Sep 2019 11:33:51 +0200},
  biburl    = {https://dblp.org/rec/journals/corr/abs-1909-08671.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{Ilya2018,
  author    = {Ilya Sergey and
               Amrit Kumar and
               Aquinas Hobor},
  title     = {Scilla: a Smart Contract Intermediate-Level LAnguage},
  journal   = {CoRR},
  volume    = {abs/1801.00687},
  year      = {2018},
  url       = {http://arxiv.org/abs/1801.00687},
  eprinttype = {arXiv},
  eprint    = {1801.00687},
  timestamp = {Tue, 17 Sep 2019 14:15:20 +0200},
  biburl    = {https://dblp.org/rec/journals/corr/abs-1801-00687.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{Annenkov2020,
author = {Annenkov, Danil and Nielsen, Jakob Botsch and Spitters, Bas},
title = {ConCert: A Smart Contract Certification Framework in Coq},
year = {2020},
isbn = {9781450370974},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3372885.3373829},
doi = {10.1145/3372885.3373829},
abstract = {We present a new way of embedding functional languages into the Coq proof assistant by using meta-programming. This allows us to develop the meta-theory of the language using the deep embedding and provides a convenient way for reasoning about concrete programs using the shallow embedding. We connect the deep and the shallow embeddings by a soundness theorem. As an instance of our approach, we develop an embedding of a core smart contract language into Coq and verify several important properties of a crowdfunding contract based on a previous formalisation of smart contract execution in blockchains.},
booktitle = {Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs},
pages = {215–228},
numpages = {14},
keywords = {Coq, blockchain, certified programming, smart contracts, software correctness, functional programming languages},
location = {New Orleans, LA, USA},
series = {CPP 2020}
}

@inproceedings{Pace2020,
author="Pace, Gordon J.
and S{\'a}nchez, C{\'e}sar
and Schneider, Gerardo",
editor="Margaria, Tiziana
and Steffen, Bernhard",
title="Reliable Smart Contracts",
booktitle="Leveraging Applications of Formal Methods, Verification and Validation: Applications",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="3--8",
abstract="The rise of smart contracts executed on blockchain and other distributed ledger technologies enabled trustless yet decentralised computation. Various applications take advantage of this computational model, including enforced financial contracts, self-sovereign identity and voting. But smart contracts are nothing but software running on a blockchain, with risks of malfunction due to bugs in the code. Compared to traditional systems, there is an additional risk in that erroneous computation or transactions triggered by a smart contract cannot be easily rolled back due to the immutability of the underlying execution model. This ISoLA track brings together a number of experts in the field of smart contract reliability and verification to discuss the state-of-the-art in smart contract dependability and discuss research challenges and future directions.",
isbn="978-3-030-61467-6"
}

@inproceedings{Hildenbrandt2018,
author={Hildenbrandt, Everett and Saxena, Manasvi and Rodrigues, Nishant and Zhu, Xiaoran and Daian, Philip and Guth, Dwight and Moore, Brandon and Park, Daejun and Zhang, Yi and Stefanescu, Andrei and Rosu, Grigore},
booktitle={2018 IEEE 31st Computer Security Foundations Symposium (CSF)},
title={KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine},
year={2018},
volume={},
number={},
pages={204-217},
doi={10.1109/CSF.2018.00022}
}

@misc{Plutus2022,
author={{IOHK}},
title={Plutus Core and Plutus Tx user guide},
year={2022},
url={https://plutus.readthedocs.io/en/latest/}
}

@paper{Zen2017,
author={{Zen Protocol Development}},
title={An Introduction to the Zen Protocol},
year={2017},
url={https://www.zenprotocol.com/en/white_paper.pdf}
}

@paper{Zilliqa2017,
author={{The \textsc{Zilliqa} Team}},
title={The \textsc{Zilliqa} Technical Paper},
year={2017},
url={https://docs.zilliqa.com/whitepaper.pdf}
}

@paper{Tezos2014,
author={{L.M Goodman}},
title={Tezos -- a self-amending crypto-ledger White paper},
year={2014},
url={https://tezos.com/whitepaper.pdf}
}

@paper{RChain2021,
author={{RChain Cooperative}},
title={RChain Whitepaper},
year={2021},
url={https://rchain.coop/whitepaper.html}
}

@misc{Rholang2021,
author={{RChain Cooperative}},
title={Rholang},
year={2022},
url={https://rholang.github.io/docs/rholang/}
}

@inproceedings{Bernardo2020,
author="Bernardo, Bruno
and Cauderlier, Rapha{\"e}l
and Pesin, Basile
and Tesson, Julien",
editor="Bernhard, Matthew
and Bracciali, Andrea
and Camp, L. Jean
and Matsuo, Shin'ichiro
and Maurushat, Alana
and R{\o}nne, Peter B.
and Sala, Massimiliano",
title="Albert, An Intermediate Smart-Contract Language for the Tezos Blockchain",
booktitle="Financial Cryptography and Data Security",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="584--598",
abstract="Tezos is a smart-contract blockchain. Tezos smart contracts are written in a low-level stack-based language called Michelson. In this article we present Albert, an intermediate language for Tezos smart contracts which abstracts Michelson stacks as linearly typed records. We also describe its compiler to Michelson, written in Coq, that targets Mi-Cho-Coq, a formal specification of Michelson implemented in Coq.",
isbn="978-3-030-54455-3"
}

@inproceedings{Pettersson2016,
  title={Safer smart contracts through type-driven development},
  author={Jack Pettersson and Robert Edstr{\"o}m},
  booktitle={Master's thesis},
  year={2016}
}

@inproceedings{Swamy2013,
author = {Swamy, Nikhil and Chen, Juan and Livshits, Ben},
title = {Verifying Higher-order Programs with the Dijkstra Monad},
booktitle = {ACM Programming Language Design and Implementation (PLDI) 2013},
year = {2013},
month = {June},
abstract = {Modern programming languages, ranging from Haskell and ML, to JavaScript, C# and Java, all make extensive use of higher-order state. This paper advocates a new verification methodology for higher-order stateful programs, based on a new monad of predicate transformers called the Dijkstra monad.
Using the Dijkstra monad has a number of benefits. First, the monad naturally yields a weakest pre-condition calculus. Second, the computed specifications are structurally simpler in several ways, e.g., single-state post-conditions are sufficient (rather than the more complex two-state post-conditions). Finally, the monad can easily be varied to handle features like exceptions and heap invariants, while retaining the same type inference algorithm.
We implement the Dijkstra monad and its type inference algorithm for the F* programming language. Our most extensive case study evaluates the Dijkstra monad and its F* implementation by using it to verify JavaScript programs.
Specifically, we describe a tool chain that translates programs in a subset of JavaScript decorated with assertions and loop invariants to F*. Once in F*, our type inference algorithm computes verification conditions and automatically discharges their proofs using an SMT solver. We use our tools to prove that a core model of the JavaScript runtime in F* respects various invariants and that a suite of JavaScript source programs are free of runtime errors.},
publisher = {ACM},
url = {https://www.microsoft.com/en-us/research/publication/verifying-higher-order-programs-with-the-dijkstra-monad/},
edition = {ACM Programming Language Design and Implementation (PLDI) 2013},
}

@article{Alechina2000,
    author = {Alechina, N and Immerman, N},
    title = "{Reachability logic: an efficient fragment of transitive closure logic}",
    journal = {Logic Journal of the IGPL},
    volume = {8},
    number = {3},
    pages = {325-337},
    year = {2000},
    month = {05},
    abstract = "{We define reachability logic (RL), a fragment of FO2(TC) (with boolean variables) that admits efficient model checking - linear time with a small constant - as a function of the size of the structure being checked. RL is expressive enough so that modal logics PDL and CTL* can be linearly embedded in it. The model checking algorithm is also linear in the size of the formula, but exponential in the number of boolean variables occurring in it. In practice this number is very small. In particular, for CTL and PDL formulas the resulting model checking algorithm remains linear. For CTL* the complexity of model checking - which is PSPACE complete in the worst case - can be read from the face of the translated formula.}",
    issn = {1367-0751},
    doi = {10.1093/jigpal/8.3.325},
    url = {https://doi.org/10.1093/jigpal/8.3.325},
    eprint = {https://academic.oup.com/jigpal/article-pdf/8/3/325/2419781/080325.pdf},
}


@inproceedings{Xiaohong2019,
title = "Matching µ-logic: Foundation of K framework",
abstract = "K framework is an effort in realizing the ideal language framework where programming languages must have formal semantics and all languages tools are automatically generated from the formal semantics in a correct-by-construction manner at no additional costs. In this extended abstract, we present matching µ-logic as the foundation of K and discuss some of its applications in defining constructors, transition systems, modal µ-logic and temporal logic variants, and reachability logic.",
keywords = "Matching µ-logic, Program verification, Reachability logic",
author = "Xiaohong Chen and Grigore Ro{\c s}u",
note = "Publisher Copyright: {\textcopyright} Xiaohong Chen and Grigore Ro{\c s}u.; 8th Conference on Algebra and Coalgebra in Computer Science, CALCO 2019 ; Conference date: 03-06-2019 Through 06-06-2019",
year = "2019",
month = nov,
doi = "10.4230/LIPIcs.CALCO.2019.1",
language = "English (US)",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
editor = "Markus Roggenbach and Ana Sokolova",
booktitle = "8th Conference on Algebra and Coalgebra in Computer Science, CALCO 2019"
}

@inproceedings{Goes2020,
author="Goes, Christopher",
editor="Margaria, Tiziana
and Steffen, Bernhard",
title="Compiling Quantitative Type Theory to Michelson for Compile-Time Verification and Run-time Efficiency in Juvix",
booktitle="Leveraging Applications of Formal Methods, Verification and Validation: Applications",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="146--160",
abstract="Michelson, the stack-based virtual machine of the Tezos blockchain, integrates type-checking for program execution completion but not program correctness. Manual stack tracking is efficient but less ergonomic to write in than a higher-level lambda calculus with variables. Compiling McBride's Quantitative Type Theory to Michelson allows for compile-time verification of semantic predicates and automatic stack optimisation by virtue of the type-theoretic usage accounting system.",
isbn="978-3-030-61467-6"
}

@article{Atkey2018,
  title={Syntax and Semantics of Quantitative Type Theory},
  author={Robert Atkey},
  journal={Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
  year={2018}
}

@paper{Delmolino2015,
author={Delmolino Kevin and Arnett Mitchell and Kosba Ahmed and Miller Andrew and Shi Elaine},
title={A Programmer’s Guide to Ethereum and Serpent},
year={2015},
url={http://mc2-umd.github.io/ethereumlab/docs/serpent_tutorial.pdf}
}

@inproceedings{Rondon2008,
  title={Liquid types},
  author={Rondon, Patrick Maxim and Kawaguchi, Ming and Jhala, Ranjit},
  booktitle={ACM-SIGPLAN Symposium on Programming Language Design and Implementation},
  year={2008}
}

@inproceedings{Feng2017,
author = {Feng, Yu and Martins, Ruben and Wang, Yuepeng and Dillig, Isil and Reps, Thomas W.},
title = {Component-Based Synthesis for Complex APIs},
year = {2017},
isbn = {9781450346603},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3009837.3009851},
doi = {10.1145/3009837.3009851},
abstract = {Component-based approaches to program synthesis assemble programs from a database of existing components, such as methods provided by an API. In this paper, we present a novel type-directed algorithm for component-based synthesis. The key novelty of our approach is the use of a compact Petri-net representation to model relationships between methods in an API. Given a target method signature S, our approach performs reachability analysis on the underlying Petri-net model to identify sequences of method calls that could be used to synthesize an implementation of S. The programs synthesized by our algorithm are guaranteed to type check and pass all test cases provided by the user. We have implemented this approach in a tool called SyPet, and used it to successfully synthesize real-world programming tasks extracted from on-line forums and existing code repositories. We also compare SyPet with two state-of-the-art synthesis tools, namely InSynth and CodeHint, and demonstrate that SyPet can synthesize more programs in less time. Finally, we compare our approach with an alternative solution based on hypergraphs and demonstrate its advantages.},
booktitle = {Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages},
pages = {599–612},
numpages = {14},
keywords = {Component-based, Petri-net, Type-directed, Program Synthesis},
location = {Paris, France},
series = {POPL '17}
}

@article{Guo2020,
author = {Guo, Zheng and James, Michael and Justo, David and Zhou, Jiaxiao and Wang, Ziteng and Jhala, Ranjit and Polikarpova, Nadia},
title = {Program Synthesis by Type-Guided Abstraction Refinement},
year = {2019},
issue_date = {January 2020},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {4},
number = {POPL},
url = {https://doi.org/10.1145/3371080},
doi = {10.1145/3371080},
abstract = {We consider the problem of type-directed component-based synthesis where, given a set of (typed) components and a query type, the goal is to synthesize a term that inhabits the query. Classical approaches based on proof search in intuitionistic logics do not scale up to the standard libraries of modern languages, which span hundreds or thousands of components. Recent graph reachability based methods proposed for Java do scale, but only apply to monomorphic data and components: polymorphic data and components infinitely explode the size of the graph that must be searched, rendering synthesis intractable. We introduce type-guided abstraction refinement (TYGAR), a new approach for scalable type-directed synthesis over polymorphic datatypes and components. Our key insight is that we can overcome the explosion by building a graph over abstract types which represent a potentially unbounded set of concrete types. We show how to use graph reachability to search for candidate terms over abstract types, and introduce a new algorithm that uses proofs of untypeability of ill-typed candidates to iteratively refine the abstraction until a well-typed result is found. We have implemented TYGAR in H+, a tool that takes as input a set of Haskell libraries and a query type, and returns a Haskell term that uses functions from the provided libraries to implement the query type. Our support for polymorphism allows H+ to work with higher-order functions and type classes, and enables more precise queries due to parametricity. We have evaluated H+ on 44 queries using a set of popular Haskell libraries with a total of 291 components. H+ returns an interesting solution within the first five results for 32 out of 44 queries. Our results show that TYGAR allows H+ to rapidly return well-typed terms, with the median time to first solution of just 1.4 seconds. Moreover, we observe that gains from iterative refinement over exhaustive enumeration are more pronounced on harder queries.},
journal = {Proc. ACM Program. Lang.},
month = {dec},
articleno = {12},
numpages = {28},
keywords = {Program Synthesis, Abstract Interpretation, Type Systems}
}

@inproceedings{Guo2022,
author = {Guo, Zheng and Cao, David and Tjong, Davin and Yang, Jean and Schlesinger, Cole and Polikarpova, Nadia},
title = {Type-Directed Program Synthesis for RESTful APIs},
year = {2022},
isbn = {9781450392655},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3519939.3523450},
doi = {10.1145/3519939.3523450},
abstract = {With the rise of software-as-a-service and microservice architectures, RESTful APIs are now ubiquitous in mobile and web applications. A service can have tens or hundreds of API methods, making it a challenge for programmers to find the right combination of methods to solve their task. We present APIphany, a component-based synthesizer for programs that compose calls to RESTful APIs. The main innovation behind APIphany is the use of precise semantic types, both to specify user intent and to direct the search. APIphany contributes three novel mechanisms to overcome challenges in adapting component-based synthesis to the REST domain: (1) a type inference algorithm for augmenting REST specifications with semantic types; (2) an efficient synthesis technique for "wrangling" semi-structured data, which is commonly required in working with RESTful APIs; and (3) a new form of simulated execution to avoid executing APIs calls during synthesis. We evaluate APIphany on three real-world APIs and 32 tasks extracted from GitHub repositories and StackOverflow. In our experiments, APIphany found correct solutions to 29 tasks, with 23 of them reported among top ten synthesis results.},
booktitle = {Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation},
pages = {122–136},
numpages = {15},
keywords = {RESTful API, Type Inference, Program Synthesis},
location = {San Diego, CA, USA},
series = {PLDI 2022}
}

@article{Michael2020,
author = {James, Michael B. and Guo, Zheng and Wang, Ziteng and Doshi, Shivani and Peleg, Hila and Jhala, Ranjit and Polikarpova, Nadia},
title = {Digging for Fold: Synthesis-Aided API Discovery for Haskell},
year = {2020},
issue_date = {November 2020},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {4},
number = {OOPSLA},
url = {https://doi.org/10.1145/3428273},
doi = {10.1145/3428273},
abstract = {We present Hoogle+, a web-based API discovery tool for Haskell. A Hoogle+ user can specify a programming task using either a type, a set of input-output tests, or both. Given a specification, the tool returns a list of matching programs composed from functions in popular Haskell libraries, and annotated with automatically-generated examples of their behavior. These features of Hoogle+ are powered by three novel techniques. First, to enable efficient type-directed synthesis from tests only, we develop an algorithm that infers likely type specifications from tests. Second, to return high-quality programs even with ambiguous specifications, we develop a technique that automatically eliminates meaningless and repetitive synthesis results. Finally, we show how to extend this elimination technique to automatically generate informative inputs that can be used to demonstrate program behavior to the user. To evaluate the effectiveness of Hoogle+ compared with traditional API search techniques, we perform a user study with 30 participants of varying Haskell proficiency. The study shows that programmers equipped with Hoogle+ generally solve tasks faster and were able to solve 50% more tasks overall.},
journal = {Proc. ACM Program. Lang.},
month = {nov},
articleno = {205},
numpages = {27},
keywords = {Program Synthesis, Type Inference, Human-Computer Interaction}
}

@misc{Mitchell2004,
author = {Mitchell Neil},
title = {Hoogle},
url = {https://hoogle.haskell.org},
year = {2004}
}

@book{Brady2017,
author={Edwin Brady},
title={Type-Driven Development with Idris},
publisher={Manning},
year={2017},
}

@inproceedings{Polikarpova2016,
author = {Polikarpova, Nadia and Kuraj, Ivan and Solar-Lezama, Armando},
title = {Program Synthesis from Polymorphic Refinement Types},
year = {2016},
isbn = {9781450342612},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/2908080.2908093},
doi = {10.1145/2908080.2908093},
abstract = {We present a method for synthesizing recursive functions that provably satisfy a given specification in the form of a polymorphic refinement type. We observe that such specifications are particularly suitable for program synthesis for two reasons. First, they offer a unique combination of expressive power and decidability, which enables automatic verification—and hence synthesis—of nontrivial programs. Second, a type-based specification for a program can often be effectively decomposed into independent specifications for its components, causing the synthesizer to consider fewer component combinations and leading to a combinatorial reduction in the size of the search space. At the core of our synthesis procedure is a newalgorithm for refinement type checking, which supports specification decomposition. We have evaluated our prototype implementation on a large set of synthesis problems and found that it exceeds the state of the art in terms of both scalability and usability. The tool was able to synthesize more complex programs than those reported in prior work (several sorting algorithms and operations on balanced search trees), as well as most of the benchmarks tackled by existing synthesizers, often starting from a more concise and intuitive user input.},
booktitle = {Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation},
pages = {522–538},
numpages = {17},
keywords = {Refinement Types, Program Synthesis, Functional Programming, Predicate Abstraction},
location = {Santa Barbara, CA, USA},
series = {PLDI '16}
}

@inproceedings{Flanagan2006,
  title={Hybrid type checking},
  author={Cormac Flanagan},
  booktitle={ACM-SIGACT Symposium on Principles of Programming Languages},
  year={2006}
}

@article{Brady2021,
  author    = {Edwin Brady},
  title     = {Idris 2: Quantitative Type Theory in Practice},
  journal   = {CoRR},
  volume    = {abs/2104.00480},
  year      = {2021},
  url       = {https://arxiv.org/abs/2104.00480},
  eprinttype = {arXiv},
  eprint    = {2104.00480},
  timestamp = {Mon, 12 Apr 2021 16:14:56 +0200},
  biburl    = {https://dblp.org/rec/journals/corr/abs-2104-00480.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inbook{Norell2009,
author="Norell, Ulf",
editor="Koopman, Pieter
and Plasmeijer, Rinus
and Swierstra, Doaitse",
title="Dependently Typed Programming in Agda",
bookTitle="Advanced Functional Programming: 6th International School, AFP 2008, Heijen, The Netherlands, May 2008, Revised Lectures",
year="2009",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="230--266",
abstract="In Hindley-Milner style languages, such as Haskell and ML, there is a clear separation between types and values. In a dependently typed language the line is more blurry - types can contain (depend on) arbitrary values and appear as arguments and results of ordinary functions.",
isbn="978-3-642-04652-0",
url="https://doi.org/10.1007/978-3-642-04652-0_5"
}

@InProceedings{Heineman2016,
author="Heineman, George T.
and Bessai, Jan
and D{\"u}dder, Boris
and Rehof, Jakob",
editor="Margaria, Tiziana
and Steffen, Bernhard",
title="A Long and Winding Road Towards Modular Synthesis",
booktitle="Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques",
year="2016",
publisher="Springer International Publishing",
address="Cham",
pages="303--317",
abstract="This paper offers a personal reflection on a number of attempts over the past decade to apply a variety of approaches to construct a product line for solitaire card games implemented in Java. A product line shares a common set of features developed from a common set of software artifacts. A feature is a unit of functionality within a system that is visible to an end-user and can be used to differentiate members of the product line. The ultimate research goal is to assemble a product line by selecting a configuration of a set of pre-designed modular units and developing new units as necessary for individual members; in short, incorporating configuration into routine development. A secondary goal was to develop a suitable tool chain that could be integrated with existing IDEs to achieve widespread acceptance of the approach. We compare progress against by-hand development in Java. During this period we investigated a number of approaches from the research literature, including components, aspects, and layers; these efforts led to a productive collaboration supported by type theory.",
isbn="978-3-319-47166-2"
}

@inproceedings{Knoth2019,
author = {Knoth, Tristan and Wang, Di and Polikarpova, Nadia and Hoffmann, Jan},
title = {Resource-Guided Program Synthesis},
year = {2019},
isbn = {9781450367127},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3314221.3314602},
doi = {10.1145/3314221.3314602},
abstract = {This article presents resource-guided synthesis, a technique for synthesizing recursive programs that satisfy both a functional specification and a symbolic resource bound. The technique is type-directed and rests upon a novel type system that combines polymorphic refinement types with potential annotations of automatic amortized resource analysis. The type system enables efficient constraint-based type checking and can express precise refinement-based resource bounds. The proof of type soundness shows that synthesized programs are correct by construction. By tightly integrating program exploration and type checking, the synthesizer can leverage the user-provided resource bound to guide the search, eagerly rejecting incomplete programs that consume too many resources. An implementation in the resource-guided synthesizer ReSyn is used to evaluate the technique on a range of recursive data structure manipulations. The experiments show that ReSyn synthesizes programs that are asymptotically more efficient than those generated by a resource-agnostic synthesizer. Moreover, synthesis with ReSyn is faster than a naive combination of synthesis and resource analysis. ReSyn is also able to generate implementations that have a constant resource consumption for fixed input sizes, which can be used to mitigate side-channel attacks.},
booktitle = {Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation},
pages = {253–268},
numpages = {16},
keywords = {Refinement Types, Automated Amortized Resource Analysis, Program Synthesis},
location = {Phoenix, AZ, USA},
series = {PLDI 2019}
}

@article{Frankle2016,
author = {Frankle, Jonathan and Osera, Peter-Michael and Walker, David and Zdancewic, Steve},
title = {Example-Directed Synthesis: A Type-Theoretic Interpretation},
year = {2016},
issue_date = {January 2016},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {51},
number = {1},
issn = {0362-1340},
url = {https://doi.org/10.1145/2914770.2837629},
doi = {10.1145/2914770.2837629},
abstract = {Input-output examples have emerged as a practical and user-friendly specification mechanism for program synthesis in many environments. While example-driven tools have demonstrated tangible impact that has inspired adoption in industry, their underlying semantics are less well-understood: what are "examples" and how do they relate to other kinds of specifications? This paper demonstrates that examples can, in general, be interpreted as refinement types. Seen in this light, program synthesis is the task of finding an inhabitant of such a type. This insight provides an immediate semantic interpretation for examples. Moreover, it enables us to exploit decades of research in type theory as well as its correspondence with intuitionistic logic rather than designing ad hoc theoretical frameworks for synthesis from scratch. We put this observation into practice by formalizing synthesis as proof search in a sequent calculus with intersection and union refinements that we prove to be sound with respect to a conventional type system. In addition, we show how to handle negative examples, which arise from user feedback or counterexample-guided loops. This theory serves as the basis for a prototype implementation that extends our core language to support ML-style algebraic data types and structurally inductive functions. Users can also specify synthesis goals using polymorphic refinements and import monomorphic libraries. The prototype serves as a vehicle for empirically evaluating a number of different strategies for resolving the nondeterminism of the sequent calculus---bottom-up theorem-proving, term enumeration with refinement type checking, and combinations of both---the results of which classify, explain, and validate the design choices of existing synthesis systems. It also provides a platform for measuring the practical value of a specification language that combines "examples" with the more general expressiveness of refinements.},
journal = {SIGPLAN Not.},
month = {jan},
pages = {802–815},
numpages = {14},
keywords = {Functional Programming, Sequent Calculus, Program Synthesis, Type Theory, Refinement Types, Proof Search}
}

@article{Warrell2016,
  title={A Probabilistic Dependent Type System based on Non-Deterministic Beta Reduction},
  author={Jonathan H. Warrell},
  journal={ArXiv},
  year={2016},
  volume={abs/1602.06420}
}

@article{Vazou2014,
author = {Vazou, Niki and Seidel, Eric L. and Jhala, Ranjit and Vytiniotis, Dimitrios and Peyton-Jones, Simon},
title = {Refinement Types for Haskell},
year = {2014},
issue_date = {September 2014},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {49},
number = {9},
issn = {0362-1340},
url = {https://doi.org/10.1145/2692915.2628161},
doi = {10.1145/2692915.2628161},
abstract = {SMT-based checking of refinement types for call-by-value languages is a well-studied subject. Unfortunately, the classical translation of refinement types to verification conditions is unsound under lazy evaluation. When checking an expression, such systems implicitly assume that all the free variables in the expression are bound to values. This property is trivially guaranteed by eager, but does not hold under lazy, evaluation. Thus, to be sound and precise, a refinement type system for Haskell and the corresponding verification conditions must take into account which subset of binders actually reduces to values. We present a stratified type system that labels binders as potentially diverging or not, and that (circularly) uses refinement types to verify the labeling. We have implemented our system in LIQUIDHASKELL and present an experimental evaluation of our approach on more than 10,000 lines of widely used Haskell libraries. We show that LIQUIDHASKELL is able to prove 96% of all recursive functions terminating, while requiring a modest 1.7 lines of termination-annotations per 100 lines of code.},
journal = {SIGPLAN Not.},
month = {aug},
pages = {269–282},
numpages = {14}
}

@inproceedings{Warrell2022,
author = {Jonathan Warrell and Alexey Potapov and Adam Vandervorst and Ben Goertzel},
year = {2022},
title = {A meta-probabilistic-programming language for bisimulation of probabilistic and non-well-founded type systems},
series = {AGI}
}

@article{Krijnen2022,
  author    = {Jacco O. G. Krijnen and
               Manuel M. T. Chakravarty and
               Gabriele Keller and
               Wouter Swierstra},
  title     = {Translation Certification for Smart Contracts},
  journal   = {CoRR},
  volume    = {abs/2201.04919},
  year      = {2022},
  url       = {https://arxiv.org/abs/2201.04919},
  eprinttype = {arXiv},
  eprint    = {2201.04919},
  timestamp = {Thu, 20 Jan 2022 14:21:35 +0100},
  biburl    = {https://dblp.org/rec/journals/corr/abs-2201-04919.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{Timothy2018,
author="Jones, Timothy
and Homer, Michael",
editor="Ryu, Sukyoung",
title="The Practice of a Compositional Functional Programming Language",
booktitle="Programming Languages and Systems",
year="2018",
publisher="Springer International Publishing",
address="Cham",
pages="166--177",
abstract="Function composition is a very natural operation, but most language paradigms provide poor support for it. Without linguistic support programmers must work around or manually implement what would be simple compositions. The Kihi language uses only composition, makes all state visible, and reduces to just six core operations. Kihi programs are easily stepped by textual reduction but provide a foundation for compositional design and analysis.",
isbn="978-3-030-02768-1"
}

@inproceedings{Caires2004,
author="Caires, Lu{\'i}s",
editor="Walukiewicz, Igor",
title="Behavioral and Spatial Observations in a Logic for the $\pi$-Calculus",
booktitle="Foundations of Software Science and Computation Structures",
year="2004",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="72--89",
abstract="In addition to behavioral properties, spatial logics can talk about other key properties of concurrent systems such as secrecy, freshness, usage of resources, and distribution. We study an expressive spatial logic for systems specified in the synchronous $\pi$-calculus with recursion, based on a small set of behavioral and spatial observations. We give coinductive and equational characterizations of the equivalence induced on processes by the logic, and conclude that it strictly lies between structural congruence and strong bisimulation. We then show that model-checking is decidable for a useful class of processes that includes the finite-control fragment of the $\pi$-calculus.",
isbn="978-3-540-24727-2"
}

@inproceedings{Williams2021,
  author    = {Christian Williams and
               Michael Stay},
  editor    = {Kohei Kishida},
  title     = {Native Type Theory},
  booktitle = {Proceedings of the Fourth International Conference on Applied Category
               Theory, {ACT} 2021, Cambridge, United Kingdom, 12-16th July 2021},
  series    = {{EPTCS}},
  volume    = {372},
  pages     = {116--132},
  year      = {2021},
  url       = {https://doi.org/10.4204/EPTCS.372.9},
  doi       = {10.4204/EPTCS.372.9},
  timestamp = {Mon, 05 Dec 2022 10:58:58 +0100},
  biburl    = {https://dblp.org/rec/journals/corr/abs-2102-04672.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{Meredith2005,
title = {A Reflective Higher-order Calculus},
journal = {Electronic Notes in Theoretical Computer Science},
volume = {141},
number = {5},
pages = {49-67},
year = {2005},
note = {Proceedings of the Workshop on the Foundations of Interactive Computation (FInCo 2005)},
issn = {1571-0661},
doi = {https://doi.org/10.1016/j.entcs.2005.05.016},
url = {https://www.sciencedirect.com/science/article/pii/S1571066105051893},
author = {L.G. Meredith and Matthias Radestock},
keywords = {concurrency, message-passing, process calculus, reflection},
abstract = {The π-calculus is not a closed theory, but rather a theory dependent upon some theory of names. Taking an operational view, one may think of the π-calculus as a procedure that when handed a theory of names provides a theory of processes that communicate over those names. This openness of the theory has been exploited in π-calculus implementations, where ancillary mechanisms provide a means of interpreting of names, e.g. as tcp/ip ports. But, foundationally, one might ask if there is a closed theory of processes, i.e. one in which the theory of names arises from and is wholly determined by the theory of processes. Here we present such a theory in the form of an asynchronous message-passing calculus built on a notion of quoting. Names are quoted processes, and as such represent the code of a process, a reification of the syntactic structure of the process as an object for process manipulation. Name- passing in this setting becomes a way of passing the code of a process as a message. In the presence of a dequote operation, turning the code of a process into a running instance, this machinery yields higher-order characteristics without the introduction of process variables. As is standard with higher-order calculi, replication and/or recursion is no longer required as a primitive operation. Somewhat more interestingly, the introduction of a process constructor to dynamically convert a process into its code is essential to obtain computational completeness, and simultaneously supplants the function of the ν operator. In fact, one may give a compositional encoding of the ν operator into a calculus featuring dynamic quote as well as dequote.}
}

@article{Duong2004,
author = {Duong, Deborah and Grefenstette, John},
year = {2004},
month = {01},
pages = {},
title = {SISTER: a Symbolic Interactionist Simulation of Trade and Emergent Roles},
volume = {8},
journal = {Journal of Artificial Societies and Social Simulation}
}

@article{Barke2020,
author = {Barke, Shraddha and Peleg, Hila and Polikarpova, Nadia},
title = {Just-in-Time Learning for Bottom-up Enumerative Synthesis},
year = {2020},
issue_date = {November 2020},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {4},
number = {OOPSLA},
url = {https://doi.org/10.1145/3428295},
doi = {10.1145/3428295},
abstract = {A key challenge in program synthesis is the astronomical size of the search space the synthesizer has to explore. In response to this challenge, recent work proposed to guide synthesis using learned probabilistic models. Obtaining such a model, however, might be infeasible for a problem domain where no high-quality training data is available. In this work we introduce an alternative approach to guided program synthesis: instead of training a model ahead of time we show how to bootstrap one just in time, during synthesis, by learning from partial solutions encountered along the way. To make the best use of the model, we also propose a new program enumeration algorithm we dub guided bottom-up search, which extends the efficient bottom-up search with guidance from probabilistic models. We implement this approach in a tool called Probe, which targets problems in the popular syntax-guided synthesis (SyGuS) format. We evaluate Probe on benchmarks from the literature and show that it achieves significant performance gains both over unguided bottom-up search and over a state-of-the-art probability-guided synthesizer, which had been trained on a corpus of existing solutions. Moreover, we show that these performance gains do not come at the cost of solution quality: programs generated by Probe are only slightly more verbose than the shortest solutions and perform no unnecessary case-splitting.},
journal = {Proc. ACM Program. Lang.},
month = {nov},
articleno = {227},
numpages = {29},
keywords = {Probabilistic models, Domain-specific languages, Program Synthesis}
}

@InProceedings{Ozkural2011,
author="{\"O}zkural, Eray",
editor="Schmidhuber, J{\"u}rgen
and Th{\'o}risson, Kristinn R.
and Looks, Moshe",
title="Towards Heuristic Algorithmic Memory",
booktitle="Artificial General Intelligence",
year="2011",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="382--387",
abstract="We propose a long-term memory design for artificial general intelligence based on Solomonoff's incremental machine learning methods. We introduce four synergistic update algorithms that use a Stochastic Context-Free Grammar as a guiding probability distribution of programs. The update algorithms accomplish adjusting production probabilities, re-using previous solutions, learning programming idioms and discovery of frequent subprograms. A controlled experiment with a long training sequence shows that our incremental learning approach is effective.",
isbn="978-3-642-22887-2"
}

@MISC{Looks2006,
author = {Moshe Looks and B. Sc and Saint Louis Missouri and Saint Louis},
title = {ABSTRACT COMPETENT PROGRAM EVOLUTION by Moshe Looks},
year = {2006}
}

@InProceedings{Franz2022,
author="Franz, Arthur",
editor="Goertzel, Ben
and Ikl{\'e}, Matthew
and Potapov, Alexey",
title="Experiments on the Generalization of Machine Learning Algorithms",
booktitle="Artificial General Intelligence",
year="2022",
publisher="Springer International Publishing",
address="Cham",
pages="75--85",
abstract="The inductive programming system WILLIAM is applied to machine learning tasks, in particular, centralization, outlier detection, linear regression, linear classification and decision tree classification. These examples appear as a special case of WILLIAM's general operation of trying to compress data without any special tuning.",
isbn="978-3-030-93758-4"
}

@INPROCEEDINGS{9793546,

  author={Jain, Naman and Vaidyanath, Skanda and Iyer, Arun and Natarajan, Nagarajan and Parthasarathy, Suresh and Rajamani, Sriram and Sharma, Rahul},

  booktitle={2022 IEEE/ACM 44th International Conference on Software Engineering (ICSE)}, 

  title={Jigsaw: Large Language Models meet Program Synthesis}, 

  year={2022},

  volume={},

  number={},

  pages={1219-1231},

  doi={10.1145/3510003.3510203}}

@inproceedings{Jain2022,
  author={Jain, Naman and Vaidyanath, Skanda and Iyer, Arun and Natarajan, Nagarajan and Parthasarathy, Suresh and Rajamani, Sriram and Sharma, Rahul},
  booktitle={2022 IEEE/ACM 44th International Conference on Software Engineering (ICSE)},
  title={Jigsaw: Large Language Models meet Program Synthesis},
  year={2022},
  pages={1219-1231},
  doi={10.1145/3510003.3510203}
}

@inproceedings{Brown2020,
author = {Brown, Tom B. and Mann, Benjamin and Ryder, Nick and Subbiah, Melanie and Kaplan, Jared and Dhariwal, Prafulla and Neelakantan, Arvind and Shyam, Pranav and Sastry, Girish and Askell, Amanda and Agarwal, Sandhini and Herbert-Voss, Ariel and Krueger, Gretchen and Henighan, Tom and Child, Rewon and Ramesh, Aditya and Ziegler, Daniel M. and Wu, Jeffrey and Winter, Clemens and Hesse, Christopher and Chen, Mark and Sigler, Eric and Litwin, Mateusz and Gray, Scott and Chess, Benjamin and Clark, Jack and Berner, Christopher and McCandlish, Sam and Radford, Alec and Sutskever, Ilya and Amodei, Dario},
title = {Language Models Are Few-Shot Learners},
year = {2020},
isbn = {9781713829546},
publisher = {Curran Associates Inc.},
address = {Red Hook, NY, USA},
abstract = {We demonstrate that scaling up language models greatly improves task-agnostic, few-shot performance, sometimes even becoming competitive with prior state-of-the-art fine-tuning approaches. Specifically, we train GPT-3, an autoregressive language model with 175 billion parameters, 10x more than any previous non-sparse language model, and test its performance in the few-shot setting. For all tasks, GPT-3 is applied without any gradient updates or fine-tuning, with tasks and few-shot demonstrations specified purely via text interaction with the model. GPT-3 achieves strong performance on many NLP datasets, including translation, question-answering, and cloze tasks. We also identify some datasets where GPT-3's few-shot learning still struggles, as well as some datasets where GPT-3 faces methodological issues related to training on large web corpora.},
booktitle = {Proceedings of the 34th International Conference on Neural Information Processing Systems},
articleno = {159},
numpages = {25},
location = {Vancouver, BC, Canada},
series = {NIPS'20}
}

@article{Chen2021,
  author    = {Mark Chen and
               Jerry Tworek and
               Heewoo Jun and
               Qiming Yuan and
               Henrique Ponde de Oliveira Pinto and
               Jared Kaplan and
               Harrison Edwards and
               Yuri Burda and
               Nicholas Joseph and
               Greg Brockman and
               Alex Ray and
               Raul Puri and
               Gretchen Krueger and
               Michael Petrov and
               Heidy Khlaaf and
               Girish Sastry and
               Pamela Mishkin and
               Brooke Chan and
               Scott Gray and
               Nick Ryder and
               Mikhail Pavlov and
               Alethea Power and
               Lukasz Kaiser and
               Mohammad Bavarian and
               Clemens Winter and
               Philippe Tillet and
               Felipe Petroski Such and
               Dave Cummings and
               Matthias Plappert and
               Fotios Chantzis and
               Elizabeth Barnes and
               Ariel Herbert{-}Voss and
               William Hebgen Guss and
               Alex Nichol and
               Alex Paino and
               Nikolas Tezak and
               Jie Tang and
               Igor Babuschkin and
               Suchir Balaji and
               Shantanu Jain and
               William Saunders and
               Christopher Hesse and
               Andrew N. Carr and
               Jan Leike and
               Joshua Achiam and
               Vedant Misra and
               Evan Morikawa and
               Alec Radford and
               Matthew Knight and
               Miles Brundage and
               Mira Murati and
               Katie Mayer and
               Peter Welinder and
               Bob McGrew and
               Dario Amodei and
               Sam McCandlish and
               Ilya Sutskever and
               Wojciech Zaremba},
  title     = {Evaluating Large Language Models Trained on Code},
  journal   = {CoRR},
  volume    = {abs/2107.03374},
  year      = {2021},
  url       = {https://arxiv.org/abs/2107.03374},
  eprinttype = {arXiv},
  eprint    = {2107.03374},
  timestamp = {Tue, 20 Jul 2021 15:08:33 +0200},
  biburl    = {https://dblp.org/rec/journals/corr/abs-2107-03374.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{Khan2023,
author = {Khan, Junaed Younus and Uddin, Gias},
title = {Automatic Code Documentation Generation Using GPT-3},
year = {2023},
isbn = {9781450394758},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3551349.3559548},
doi = {10.1145/3551349.3559548},
abstract = {Source code documentation is an important artifact for efficient software development. Code documentation could greatly benefit from automation since manual documentation is often labouring, resource and time-intensive. In this paper, we employed Codex for automatic code documentation creation. Codex is a GPT-3 based model pre-trained on both natural and programming languages. We find that Codex outperforms existing techniques even with basic settings like one-shot learning (i.e., providing only one example for training). Codex achieves an overall BLEU score of 20.6 for six different programming languages (11.2% improvement over earlier state-of-the-art techniques). Thus, Codex shows promise and warrants in-depth future studies for automatic code documentation generation to support diverse development tasks.},
booktitle = {Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering},
articleno = {174},
numpages = {6},
keywords = {code documentation, GPT-3, Machine Learning.},
location = {Rochester, MI, USA},
series = {ASE '22}
}
